Loading...
机构名称:
¥ 2.0

b 互斥,可以按任何顺序执行,但不能并发;在右侧,a 和 b 之间存在真正的并发,用 HDA 语义的实心方块表示。在交错语义中,两个网之间没有区别,两者都产生左侧的转换系统。van Glabbeek 在 [31] 中首次探讨了 Petri 网和 HDA 之间的关系,其中 HDA 被定义为带标签的前立方体集,其单元是不同维度的超立方体。最近,[13] 为 HDA 引入了一种基于事件的设置,将其单元定义为带标签事件的全序集。该框架导致了 HDA 理论的许多新发展 [4,5,14,16],因此我们在这里着手将 van Glabbeek 的翻译更新为这种基于事件的设置。Petri 网是一个强大的模型,可以表示无限系统,同时保留可达性 [25] 和可覆盖性 [23] 的可判定性。尽管 Petri 网具有表达能力,但它缺少一些表示程序执行所必需的特性。在 [17] 中,作者引入了抑制弧,当通过抑制弧连接到 t 的位置不为空时,它可以防止转换 t 触发。显然,这种构造允许实现零测试,这使得带有抑制弧的 Petri 网具有图灵能力。我们研究了带有抑制弧的 Petri 网的并发语义,表明 [21] 的后验语义再次产生了 HDA。然而,对于更自由的先验语义(再次参见 [21]),我们需要引入部分 HDA,其中一些单元可能缺失,模仿现在禁止某些并发执行序列化的事实。我们进一步将我们的工作扩展到 [11] 的广义自修改网,将它们的并发语义定义为 ST 自动机,而 ST 自动机本身又概括了部分 HDA。我们开发了一个原型工具,它实现了从 Petri 网到 HDA 的转换以及从 PNI 到部分 HDA 的转换。4 我们的实现能够以模块化方式处理标准、加权和抑制弧。本文的结构如下。我们在第 2 和第 3 节开始回顾 HDA 和 Petri 网,重点介绍它们的并发语义,这种语义允许多个转换同时触发。以下各节介绍了我们的适当贡献。在第 4 节中,我们介绍了基于 [31] 的从 Petri 网到 HDA 的转换。为了克服这样构建的 HDA 的对称性,第 5 节引入了事件顺序,避免了构造中的阶乘爆炸。我们还给出了几个例子来说明 HDA 语义中的细节。然后,我们在第 6 节中考虑了具有抑制弧的 Petri 网(后验和先验语义),在第 7 节中考虑了广义自修改网。第 8 节介绍了我们的实现。

arXiv:2502.02354v1 [cs.LO] 2025 年 2 月 4 日

arXiv:2502.02354v1 [cs.LO] 2025 年 2 月 4 日PDF文件第1页

arXiv:2502.02354v1 [cs.LO] 2025 年 2 月 4 日PDF文件第2页

arXiv:2502.02354v1 [cs.LO] 2025 年 2 月 4 日PDF文件第3页

arXiv:2502.02354v1 [cs.LO] 2025 年 2 月 4 日PDF文件第4页

arXiv:2502.02354v1 [cs.LO] 2025 年 2 月 4 日PDF文件第5页

相关文件推荐